e:rvc(l,tg,v).P(e;v) == e:E. ((isrcv(e)) & lnk(e) = l & tag(e) = tg & P(e;val(e))) 

latex

---

clarification:

es-er(es; l; tg; e,v.P(e;v))
== e:es-E(es)
== ((es-isrcv(es; e))
== & es-lnk(es; e) = l  IdLnk
== & es-tag(es; e) = tg  Id
== & P(e;es-val(es; e))) 

latex

Definitions	x:A. B(x), E, b, isrcv(e), IdLnk, lnk(e), P & Q, Id, tag(e), val(e)
FDL editor aliases	es-er